Nuprl Lemma : m-sys-at-feasible
0,22
postcript
pdf
i
:Id,
A
:MsgA. Feasible(
A
)
Feasible(@
i
:
A
)
latex
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
a
=
b
,
@
i
:
A
,
Prop
,
(@
i
M
)
Lemmas
Id
wf
,
msga
wf
,
ma-feasible
wf
,
m-at-feasible
origin
i:Id, A:MsgA. Feasible(A) 
Feasible(@i: A) i:Id, A:MsgA. Feasible(A) Feasible(@i: A) 
T Qx:A. B(x)